Termination proof of /tmp/tmpMIndRL/Ex4

Termination of the following Term Rewriting System could not be shown:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

The replacement map contains the following entries:

and: {1, 2}
tt: empty set
isNatIList: empty set
isNatList: empty set
isNat: empty set
0: empty set
s: {1}
length: {1}
zeros: empty set
cons: {1}
nil: empty set
take: {1, 2}
uTake1: {1}
uTake2: {1}
uLength: {1}

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Context-sensitive rewrite system:
The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

The replacement map contains the following entries:

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {and, s, length, take, uTake1, AND, UTAKE1, TAKE, LENGTH} are replacing on all positions.
For all symbols f in {cons, uTake2, uLength, UTAKE2, ULENGTH} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNATLIST, ISNATILIST, ISNAT, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

ISNATILIST(IL) → ISNATLIST(IL)
ISNAT(s(N)) → ISNAT(N)
ISNAT(length(L)) → ISNATLIST(L)
ISNATILIST(cons(N, IL)) → AND(isNat(N), isNatIList(IL))
ISNATILIST(cons(N, IL)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)
ISNATLIST(cons(N, L)) → AND(isNat(N), isNatList(L))
ISNATLIST(cons(N, L)) → ISNAT(N)
ISNATLIST(cons(N, L)) → ISNATLIST(L)
ISNATLIST(take(N, IL)) → AND(isNat(N), isNatIList(IL))
ISNATLIST(take(N, IL)) → ISNAT(N)
ISNATLIST(take(N, IL)) → ISNATILIST(IL)
TAKE(0, IL) → UTAKE1(isNatIList(IL))
TAKE(0, IL) → ISNATILIST(IL)
TAKE(s(M), cons(N, IL)) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
TAKE(s(M), cons(N, IL)) → AND(isNat(M), and(isNat(N), isNatIList(IL)))
TAKE(s(M), cons(N, IL)) → ISNAT(M)
TAKE(s(M), cons(N, IL)) → AND(isNat(N), isNatIList(IL))
TAKE(s(M), cons(N, IL)) → ISNAT(N)
TAKE(s(M), cons(N, IL)) → ISNATILIST(IL)
LENGTH(cons(N, L)) → ULENGTH(and(isNat(N), isNatList(L)), L)
LENGTH(cons(N, L)) → AND(isNat(N), isNatList(L))
LENGTH(cons(N, L)) → ISNAT(N)
LENGTH(cons(N, L)) → ISNATLIST(L)
ULENGTH(tt, L) → LENGTH(L)

The collapsing dependency pairs are DP_c:

UTAKE2(tt, M, N, IL) → N
ULENGTH(tt, L) → L

The hidden terms of R are:

zeros
take(M, IL)

Every hiding context is built from:

take on positions {1, 2}

Hence, the new unhiding pairs DP_u are :

UTAKE2(tt, M, N, IL) → U(N)
ULENGTH(tt, L) → U(L)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(zeros) → ZEROS
U(take(M, IL)) → TAKE(M, IL)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 3 SCCs with 15 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSUsableRulesProof

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {and, s, length, take, uTake1} are replacing on all positions.
For all symbols f in {cons, uTake2, uLength} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, ISNAT, ISNATLIST, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(N, L)) → ISNAT(N)
ISNAT(s(N)) → ISNAT(N)
ISNAT(length(L)) → ISNATLIST(L)
ISNATLIST(cons(N, L)) → ISNATLIST(L)
ISNATLIST(take(N, IL)) → ISNAT(N)
ISNATLIST(take(N, IL)) → ISNATILIST(IL)
ISNATILIST(IL) → ISNATLIST(IL)
ISNATILIST(cons(N, IL)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.

The following rules are not useable and can be deleted:

and(tt, x0) → x0
isNatIList(x0) → isNatList(x0)
isNat(0) → tt
isNat(s(x0)) → isNat(x0)
isNat(length(x0)) → isNatList(x0)
isNatIList(zeros) → tt
isNatIList(cons(x0, x1)) → and(isNat(x0), isNatIList(x1))
isNatList(nil) → tt
isNatList(cons(x0, x1)) → and(isNat(x0), isNatList(x1))
isNatList(take(x0, x1)) → and(isNat(x0), isNatIList(x1))
zeros → cons(0, zeros)
take(0, x0) → uTake1(isNatIList(x0))
uTake1(tt) → nil
take(s(x0), cons(x1, x2)) → uTake2(and(isNat(x0), and(isNat(x1), isNatIList(x2))), x0, x1, x2)
uTake2(tt, x0, x1, x2) → cons(x1, take(x0, x2))
length(cons(x0, x1)) → uLength(and(isNat(x0), isNatList(x1)), x1)
uLength(tt, x0) → s(length(x0))

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSUsableRulesProof

              ↳ QCSDP

                ↳ QCSDPReductionPairProof

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, take} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {ISNAT, ISNATLIST, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(N, L)) → ISNAT(N)
ISNAT(s(N)) → ISNAT(N)
ISNAT(length(L)) → ISNATLIST(L)
ISNATLIST(cons(N, L)) → ISNATLIST(L)
ISNATLIST(take(N, IL)) → ISNAT(N)
ISNATLIST(take(N, IL)) → ISNATILIST(IL)
ISNATILIST(IL) → ISNATLIST(IL)
ISNATILIST(cons(N, IL)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)

R is empty.
Q is empty.

Using the order
Polynomial interpretation [25]:

POL(ISNAT(x₁)) = x₁
POL(ISNATILIST(x₁)) = 1 + 2·x₁
POL(ISNATLIST(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(length(x₁)) = 2 + 2·x₁
POL(s(x₁)) = 2 + 2·x₁
POL(take(x₁, x₂)) = 1 + x₁ + 2·x₂

the following usable rules
none

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISNATLIST(cons(N, L)) → ISNAT(N)
ISNAT(s(N)) → ISNAT(N)
ISNAT(length(L)) → ISNATLIST(L)
ISNATLIST(cons(N, L)) → ISNATLIST(L)
ISNATLIST(take(N, IL)) → ISNAT(N)
ISNATLIST(take(N, IL)) → ISNATILIST(IL)
ISNATILIST(IL) → ISNATLIST(IL)
ISNATILIST(cons(N, IL)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)

could be oriented strictly and thus removed.
All pairs have been removed.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSUsableRulesProof

              ↳ QCSDP

                ↳ QCSDPReductionPairProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:

The TRS P consists of the following rules:
none

R is empty.
Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {and, s, length, take, uTake1, TAKE} are replacing on all positions.
For all symbols f in {cons, uTake2, uLength, UTAKE2} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, U} are not replacing on any position.

The TRS P consists of the following rules:

TAKE(s(M), cons(N, IL)) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
UTAKE2(tt, M, N, IL) → U(N)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(take(M, IL)) → TAKE(M, IL)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

TAKE(s(M), cons(N, IL)) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(take(M, IL)) → TAKE(M, IL)

The remaining pairs can at least be oriented weakly.

UTAKE2(tt, M, N, IL) → U(N)

Used ordering: Combined order from the following AFS and order.
UTAKE2(x1, x2, x3, x4) = x3
TAKE(x1, x2) = x2
U(x1) = x1

Subterm Order

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {and, s, length, take, uTake1} are replacing on all positions.
For all symbols f in {cons, uTake2, uLength, UTAKE2} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat, U} are not replacing on any position.

The TRS P consists of the following rules:

UTAKE2(tt, M, N, IL) → U(N)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

            ↳ ConvertedToQDPProblemProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {and, s, length, take, uTake1, LENGTH} are replacing on all positions.
For all symbols f in {cons, uTake2, uLength, ULENGTH} we have µ(f) = {1}.
The symbols in {isNatIList, isNatList, isNat} are not replacing on any position.

The TRS P consists of the following rules:

ULENGTH(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → ULENGTH(and(isNat(N), isNatList(L)), L)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.

Converted QDP Problem, but could not keep Q or minimality.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

            ↳ ConvertedToQDPProblemProof

              ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ULENGTH(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → ULENGTH(and(isNat(N), isNatList(L)), L)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.
We have to consider all (P,Q,R)-chains.
We applied the Incomplete Giesl Middeldorp transformation [11] to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

  ↳ Trivial-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

TAKEACTIVE(s(M), cons(N, IL)) → ISNATILISTACTIVE(IL)
TAKEACTIVE(s(M), cons(N, IL)) → UTAKE2ACTIVE(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
MARK(take(x1, x2)) → MARK(x2)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(uTake2(x1, x2, x3, x4)) → UTAKE2ACTIVE(mark(x1), x2, x3, x4)
MARK(cons(x1, x2)) → MARK(x1)
MARK(uTake1(x1)) → UTAKE1ACTIVE(mark(x1))
ISNATLISTACTIVE(take(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
MARK(zeros) → ZEROSACTIVE
MARK(length(x1)) → MARK(x1)
ANDACTIVE(tt, T) → MARK(T)
UTAKE2ACTIVE(tt, M, N, IL) → MARK(N)
MARK(uTake2(x1, x2, x3, x4)) → MARK(x1)
ISNATLISTACTIVE(take(N, IL)) → ISNATILISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
MARK(and(x1, x2)) → MARK(x1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(take(x1, x2)) → MARK(x1)
TAKEACTIVE(0, IL) → UTAKE1ACTIVE(isNatIListActive(IL))
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL)))
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)
TAKEACTIVE(s(M), cons(N, IL)) → ISNATACTIVE(M)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
MARK(uLength(x1, x2)) → ULENGTHACTIVE(mark(x1), x2)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
MARK(uLength(x1, x2)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → ULENGTHACTIVE(andActive(isNatActive(N), isNatListActive(L)), L)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
TAKEACTIVE(s(M), cons(N, IL)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ISNATACTIVE(N)
ULENGTHACTIVE(tt, L) → MARK(L)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ULENGTHACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(uTake1(x1)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
TAKEACTIVE(0, IL) → ISNATILISTACTIVE(IL)
ISNATLISTACTIVE(take(N, IL)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

TAKEACTIVE(s(M), cons(N, IL)) → ISNATILISTACTIVE(IL)
TAKEACTIVE(s(M), cons(N, IL)) → UTAKE2ACTIVE(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
MARK(take(x1, x2)) → MARK(x2)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(uTake2(x1, x2, x3, x4)) → UTAKE2ACTIVE(mark(x1), x2, x3, x4)
MARK(cons(x1, x2)) → MARK(x1)
MARK(uTake1(x1)) → UTAKE1ACTIVE(mark(x1))
ISNATLISTACTIVE(take(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
MARK(zeros) → ZEROSACTIVE
MARK(length(x1)) → MARK(x1)
ANDACTIVE(tt, T) → MARK(T)
UTAKE2ACTIVE(tt, M, N, IL) → MARK(N)
MARK(uTake2(x1, x2, x3, x4)) → MARK(x1)
ISNATLISTACTIVE(take(N, IL)) → ISNATILISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
MARK(and(x1, x2)) → MARK(x1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(take(x1, x2)) → MARK(x1)
TAKEACTIVE(0, IL) → UTAKE1ACTIVE(isNatIListActive(IL))
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL)))
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)
TAKEACTIVE(s(M), cons(N, IL)) → ISNATACTIVE(M)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
MARK(uLength(x1, x2)) → ULENGTHACTIVE(mark(x1), x2)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
MARK(uLength(x1, x2)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → ULENGTHACTIVE(andActive(isNatActive(N), isNatListActive(L)), L)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
TAKEACTIVE(s(M), cons(N, IL)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ISNATACTIVE(N)
ULENGTHACTIVE(tt, L) → MARK(L)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ULENGTHACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(uTake1(x1)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
TAKEACTIVE(0, IL) → ISNATILISTACTIVE(IL)
ISNATLISTACTIVE(take(N, IL)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

TAKEACTIVE(s(M), cons(N, IL)) → ISNATILISTACTIVE(IL)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
TAKEACTIVE(s(M), cons(N, IL)) → UTAKE2ACTIVE(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
MARK(take(x1, x2)) → MARK(x2)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)
MARK(uTake2(x1, x2, x3, x4)) → UTAKE2ACTIVE(mark(x1), x2, x3, x4)
ISNATLISTACTIVE(take(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
MARK(length(x1)) → MARK(x1)
ANDACTIVE(tt, T) → MARK(T)
UTAKE2ACTIVE(tt, M, N, IL) → MARK(N)
MARK(uTake2(x1, x2, x3, x4)) → MARK(x1)
ISNATLISTACTIVE(take(N, IL)) → ISNATILISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
MARK(and(x1, x2)) → MARK(x1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(take(x1, x2)) → MARK(x1)
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL)))
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)
TAKEACTIVE(s(M), cons(N, IL)) → ISNATACTIVE(M)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
MARK(uLength(x1, x2)) → ULENGTHACTIVE(mark(x1), x2)
MARK(uLength(x1, x2)) → MARK(x1)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
LENGTHACTIVE(cons(N, L)) → ULENGTHACTIVE(andActive(isNatActive(N), isNatListActive(L)), L)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
TAKEACTIVE(s(M), cons(N, IL)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ISNATACTIVE(N)
ULENGTHACTIVE(tt, L) → MARK(L)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ULENGTHACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(uTake1(x1)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATLISTACTIVE(take(N, IL)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
TAKEACTIVE(0, IL) → ISNATILISTACTIVE(IL)
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

TAKEACTIVE(s(M), cons(N, IL)) → ISNATILISTACTIVE(IL)
TAKEACTIVE(s(M), cons(N, IL)) → UTAKE2ACTIVE(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
MARK(take(x1, x2)) → MARK(x2)
MARK(uTake2(x1, x2, x3, x4)) → UTAKE2ACTIVE(mark(x1), x2, x3, x4)
MARK(uTake2(x1, x2, x3, x4)) → MARK(x1)
MARK(take(x1, x2)) → MARK(x1)
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL)))
TAKEACTIVE(s(M), cons(N, IL)) → ISNATACTIVE(M)
TAKEACTIVE(s(M), cons(N, IL)) → ISNATACTIVE(N)
MARK(uTake1(x1)) → MARK(x1)
TAKEACTIVE(0, IL) → ISNATILISTACTIVE(IL)
TAKEACTIVE(s(M), cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))

The remaining pairs can at least be oriented weakly.

MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(take(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
MARK(length(x1)) → MARK(x1)
ANDACTIVE(tt, T) → MARK(T)
UTAKE2ACTIVE(tt, M, N, IL) → MARK(N)
ISNATLISTACTIVE(take(N, IL)) → ISNATILISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
MARK(and(x1, x2)) → MARK(x1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
MARK(uLength(x1, x2)) → ULENGTHACTIVE(mark(x1), x2)
MARK(uLength(x1, x2)) → MARK(x1)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
LENGTHACTIVE(cons(N, L)) → ULENGTHACTIVE(andActive(isNatActive(N), isNatListActive(L)), L)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ISNATACTIVE(N)
ULENGTHACTIVE(tt, L) → MARK(L)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ULENGTHACTIVE(tt, L) → LENGTHACTIVE(mark(L))
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATLISTACTIVE(take(N, IL)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₂
POL(ISNATACTIVE(x₁)) = 0
POL(ISNATILISTACTIVE(x₁)) = 0
POL(ISNATLISTACTIVE(x₁)) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(MARK(x₁)) = x₁
POL(TAKEACTIVE(x₁, x₂)) = 1 + x₂
POL(ULENGTHACTIVE(x₁, x₂)) = x₂
POL(UTAKE2ACTIVE(x₁, x₂, x₃, x₄)) = x₃
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = 0
POL(isNatIListActive(x₁)) = 0
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = x₁
POL(lengthActive(x₁)) = x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + x₁ + x₂
POL(takeActive(x₁, x₂)) = 1 + x₁ + x₂
POL(tt) = 0
POL(uLength(x₁, x₂)) = x₁ + x₂
POL(uLengthActive(x₁, x₂)) = x₁ + x₂
POL(uTake1(x₁)) = 1 + x₁
POL(uTake1Active(x₁)) = 1 + x₁
POL(uTake2(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₃ + x₄
POL(uTake2Active(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₃ + x₄
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

isNatActive(x1) → isNat(x1)
isNatIListActive(x1) → isNatIList(x1)
zerosActive → zeros
mark(zeros) → zerosActive
isNatListActive(x1) → isNatList(x1)
uTake1Active(x1) → uTake1(x1)
mark(uTake1(x1)) → uTake1Active(mark(x1))
takeActive(x1, x2) → take(x1, x2)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
andActive(x1, x2) → and(x1, x2)
zerosActive → cons(0, zeros)
uTake1Active(tt) → nil
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uLengthActive(tt, L) → s(lengthActive(mark(L)))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
isNatActive(length(L)) → isNatListActive(L)
mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatList(x1)) → isNatListActive(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(s(N)) → isNatActive(N)
andActive(tt, T) → mark(T)
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(take(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(length(x1)) → MARK(x1)
UTAKE2ACTIVE(tt, M, N, IL) → MARK(N)
ISNATLISTACTIVE(take(N, IL)) → ISNATILISTACTIVE(IL)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(and(x1, x2)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
MARK(uLength(x1, x2)) → ULENGTHACTIVE(mark(x1), x2)
MARK(uLength(x1, x2)) → MARK(x1)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
LENGTHACTIVE(cons(N, L)) → ULENGTHACTIVE(andActive(isNatActive(N), isNatListActive(L)), L)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ISNATACTIVE(N)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ULENGTHACTIVE(tt, L) → MARK(L)
ULENGTHACTIVE(tt, L) → LENGTHACTIVE(mark(L))
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
ISNATLISTACTIVE(take(N, IL)) → ISNATACTIVE(N)
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(take(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
MARK(length(x1)) → MARK(x1)
ANDACTIVE(tt, T) → MARK(T)
ISNATLISTACTIVE(take(N, IL)) → ISNATILISTACTIVE(IL)
MARK(and(x1, x2)) → MARK(x1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
MARK(uLength(x1, x2)) → ULENGTHACTIVE(mark(x1), x2)
MARK(uLength(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
LENGTHACTIVE(cons(N, L)) → ULENGTHACTIVE(andActive(isNatActive(N), isNatListActive(L)), L)
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ISNATACTIVE(N)
ULENGTHACTIVE(tt, L) → MARK(L)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ULENGTHACTIVE(tt, L) → LENGTHACTIVE(mark(L))
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
ISNATLISTACTIVE(take(N, IL)) → ISNATACTIVE(N)
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(length(x1)) → MARK(x1)
MARK(uLength(x1, x2)) → ULENGTHACTIVE(mark(x1), x2)
MARK(uLength(x1, x2)) → MARK(x1)

The remaining pairs can at least be oriented weakly.

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(take(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATLISTACTIVE(take(N, IL)) → ISNATILISTACTIVE(IL)
MARK(and(x1, x2)) → MARK(x1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
LENGTHACTIVE(cons(N, L)) → ULENGTHACTIVE(andActive(isNatActive(N), isNatListActive(L)), L)
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ISNATACTIVE(N)
ULENGTHACTIVE(tt, L) → MARK(L)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ULENGTHACTIVE(tt, L) → LENGTHACTIVE(mark(L))
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
ISNATLISTACTIVE(take(N, IL)) → ISNATACTIVE(N)
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₂
POL(ISNATACTIVE(x₁)) = 0
POL(ISNATILISTACTIVE(x₁)) = 0
POL(ISNATLISTACTIVE(x₁)) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(MARK(x₁)) = x₁
POL(ULENGTHACTIVE(x₁, x₂)) = x₂
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = 0
POL(isNatIListActive(x₁)) = 0
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = 1 + x₁
POL(lengthActive(x₁)) = 1 + x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = x₂
POL(takeActive(x₁, x₂)) = x₂
POL(tt) = 0
POL(uLength(x₁, x₂)) = 1 + x₁ + x₂
POL(uLengthActive(x₁, x₂)) = 1 + x₁ + x₂
POL(uTake1(x₁)) = 0
POL(uTake1Active(x₁)) = 0
POL(uTake2(x₁, x₂, x₃, x₄)) = x₃ + x₄
POL(uTake2Active(x₁, x₂, x₃, x₄)) = x₃ + x₄
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

isNatActive(x1) → isNat(x1)
isNatIListActive(x1) → isNatIList(x1)
zerosActive → zeros
mark(zeros) → zerosActive
isNatListActive(x1) → isNatList(x1)
uTake1Active(x1) → uTake1(x1)
mark(uTake1(x1)) → uTake1Active(mark(x1))
takeActive(x1, x2) → take(x1, x2)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
andActive(x1, x2) → and(x1, x2)
zerosActive → cons(0, zeros)
uTake1Active(tt) → nil
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uLengthActive(tt, L) → s(lengthActive(mark(L)))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
isNatActive(length(L)) → isNatListActive(L)
mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatList(x1)) → isNatListActive(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(s(N)) → isNatActive(N)
andActive(tt, T) → mark(T)
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(take(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATLISTACTIVE(take(N, IL)) → ISNATILISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
LENGTHACTIVE(cons(N, L)) → ULENGTHACTIVE(andActive(isNatActive(N), isNatListActive(L)), L)
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
LENGTHACTIVE(cons(N, L)) → ISNATACTIVE(N)
ULENGTHACTIVE(tt, L) → MARK(L)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ULENGTHACTIVE(tt, L) → LENGTHACTIVE(mark(L))
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATLISTACTIVE(take(N, IL)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 4 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
MARK(s(x1)) → MARK(x1)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
MARK(cons(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(take(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATLISTACTIVE(take(N, IL)) → ISNATILISTACTIVE(IL)
ISNATLISTACTIVE(take(N, IL)) → ISNATACTIVE(N)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(and(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ISNATLISTACTIVE(take(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATLISTACTIVE(take(N, IL)) → ISNATILISTACTIVE(IL)
ISNATLISTACTIVE(take(N, IL)) → ISNATACTIVE(N)

The remaining pairs can at least be oriented weakly.

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
MARK(s(x1)) → MARK(x1)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
MARK(cons(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(and(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₂
POL(ISNATACTIVE(x₁)) = x₁
POL(ISNATILISTACTIVE(x₁)) = x₁
POL(ISNATLISTACTIVE(x₁)) = x₁
POL(MARK(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = x₁
POL(isNatIList(x₁)) = x₁
POL(isNatIListActive(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = x₁
POL(length(x₁)) = x₁
POL(lengthActive(x₁)) = x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + x₁ + x₂
POL(takeActive(x₁, x₂)) = 1 + x₁ + x₂
POL(tt) = 0
POL(uLength(x₁, x₂)) = x₂
POL(uLengthActive(x₁, x₂)) = x₂
POL(uTake1(x₁)) = 0
POL(uTake1Active(x₁)) = 0
POL(uTake2(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄
POL(uTake2Active(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

isNatActive(x1) → isNat(x1)
isNatIListActive(x1) → isNatIList(x1)
zerosActive → zeros
mark(zeros) → zerosActive
isNatListActive(x1) → isNatList(x1)
uTake1Active(x1) → uTake1(x1)
mark(uTake1(x1)) → uTake1Active(mark(x1))
takeActive(x1, x2) → take(x1, x2)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
andActive(x1, x2) → and(x1, x2)
zerosActive → cons(0, zeros)
uTake1Active(tt) → nil
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uLengthActive(tt, L) → s(lengthActive(mark(L)))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
isNatActive(length(L)) → isNatListActive(L)
mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatList(x1)) → isNatListActive(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(s(N)) → isNatActive(N)
andActive(tt, T) → mark(T)
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
MARK(s(x1)) → MARK(x1)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
MARK(cons(x1, x2)) → MARK(x1)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(cons(x1, x2)) → MARK(x1)

The remaining pairs can at least be oriented weakly.

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
MARK(s(x1)) → MARK(x1)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₂
POL(ISNATACTIVE(x₁)) = 0
POL(ISNATILISTACTIVE(x₁)) = 0
POL(ISNATLISTACTIVE(x₁)) = 0
POL(MARK(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 1 + x₁
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = 0
POL(isNatIListActive(x₁)) = 0
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = 0
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + x₂
POL(takeActive(x₁, x₂)) = 1 + x₂
POL(tt) = 0
POL(uLength(x₁, x₂)) = 0
POL(uLengthActive(x₁, x₂)) = 0
POL(uTake1(x₁)) = 0
POL(uTake1Active(x₁)) = 0
POL(uTake2(x₁, x₂, x₃, x₄)) = 1 + x₃
POL(uTake2Active(x₁, x₂, x₃, x₄)) = 1 + x₃
POL(zeros) = 1
POL(zerosActive) = 1

The following usable rules [17] were oriented:

isNatActive(x1) → isNat(x1)
isNatIListActive(x1) → isNatIList(x1)
zerosActive → zeros
mark(zeros) → zerosActive
isNatListActive(x1) → isNatList(x1)
uTake1Active(x1) → uTake1(x1)
mark(uTake1(x1)) → uTake1Active(mark(x1))
takeActive(x1, x2) → take(x1, x2)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
andActive(x1, x2) → and(x1, x2)
zerosActive → cons(0, zeros)
uTake1Active(tt) → nil
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uLengthActive(tt, L) → s(lengthActive(mark(L)))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
isNatActive(length(L)) → isNatListActive(L)
mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatList(x1)) → isNatListActive(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(s(N)) → isNatActive(N)
andActive(tt, T) → mark(T)
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
MARK(s(x1)) → MARK(x1)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ISNATILISTACTIVE(IL) → ISNATLISTACTIVE(IL)
ISNATILISTACTIVE(cons(N, IL)) → ISNATACTIVE(N)

The remaining pairs can at least be oriented weakly.

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
MARK(s(x1)) → MARK(x1)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₂
POL(ISNATACTIVE(x₁)) = x₁
POL(ISNATILISTACTIVE(x₁)) = 1 + x₁
POL(ISNATLISTACTIVE(x₁)) = x₁
POL(MARK(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = x₁
POL(isNatIList(x₁)) = 1 + x₁
POL(isNatIListActive(x₁)) = 1 + x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = x₁
POL(length(x₁)) = x₁
POL(lengthActive(x₁)) = x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + x₁ + x₂
POL(takeActive(x₁, x₂)) = 1 + x₁ + x₂
POL(tt) = 0
POL(uLength(x₁, x₂)) = x₂
POL(uLengthActive(x₁, x₂)) = x₂
POL(uTake1(x₁)) = x₁
POL(uTake1Active(x₁)) = x₁
POL(uTake2(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄
POL(uTake2Active(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

isNatActive(x1) → isNat(x1)
isNatIListActive(x1) → isNatIList(x1)
zerosActive → zeros
mark(zeros) → zerosActive
isNatListActive(x1) → isNatList(x1)
uTake1Active(x1) → uTake1(x1)
mark(uTake1(x1)) → uTake1Active(mark(x1))
takeActive(x1, x2) → take(x1, x2)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
andActive(x1, x2) → and(x1, x2)
zerosActive → cons(0, zeros)
uTake1Active(tt) → nil
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uLengthActive(tt, L) → s(lengthActive(mark(L)))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
isNatActive(length(L)) → isNatListActive(L)
mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatList(x1)) → isNatListActive(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(s(N)) → isNatActive(N)
andActive(tt, T) → mark(T)
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)
MARK(s(x1)) → MARK(x1)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ISNATACTIVE(length(L)) → ISNATLISTACTIVE(L)

The remaining pairs can at least be oriented weakly.

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₂
POL(ISNATACTIVE(x₁)) = x₁
POL(ISNATILISTACTIVE(x₁)) = x₁
POL(ISNATLISTACTIVE(x₁)) = x₁
POL(MARK(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = x₁
POL(isNatIList(x₁)) = x₁
POL(isNatIListActive(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = x₁
POL(length(x₁)) = 1 + x₁
POL(lengthActive(x₁)) = 1 + x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = x₁ + x₂
POL(takeActive(x₁, x₂)) = x₁ + x₂
POL(tt) = 0
POL(uLength(x₁, x₂)) = 1 + x₂
POL(uLengthActive(x₁, x₂)) = 1 + x₂
POL(uTake1(x₁)) = 0
POL(uTake1Active(x₁)) = 0
POL(uTake2(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄
POL(uTake2Active(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

isNatActive(x1) → isNat(x1)
isNatIListActive(x1) → isNatIList(x1)
zerosActive → zeros
mark(zeros) → zerosActive
isNatListActive(x1) → isNatList(x1)
uTake1Active(x1) → uTake1(x1)
mark(uTake1(x1)) → uTake1Active(mark(x1))
takeActive(x1, x2) → take(x1, x2)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
andActive(x1, x2) → and(x1, x2)
zerosActive → cons(0, zeros)
uTake1Active(tt) → nil
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uLengthActive(tt, L) → s(lengthActive(mark(L)))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
isNatActive(length(L)) → isNatListActive(L)
mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatList(x1)) → isNatListActive(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(s(N)) → isNatActive(N)
andActive(tt, T) → mark(T)
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATACTIVE(s(N)) → ISNATACTIVE(N)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
ISNATLISTACTIVE(cons(N, L)) → ISNATACTIVE(N)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                    ↳ QDP

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATACTIVE(s(N)) → ISNATACTIVE(N)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ QDPSizeChangeProof

                                                    ↳ QDP

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATACTIVE(s(N)) → ISNATACTIVE(N)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ISNATACTIVE(s(N)) → ISNATACTIVE(N)
The graph contains the following edges 1 > 1

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(and(x1, x2)) → MARK(x1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
MARK(and(x1, x2)) → MARK(x2)
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNATILISTACTIVE(cons(N, IL)) → ANDACTIVE(isNatActive(N), isNatIListActive(IL)) at position [0] we obtained the following new rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
ISNATILISTACTIVE(cons(x0, y1)) → ANDACTIVE(isNat(x0), isNatIListActive(y1))

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
ISNATILISTACTIVE(cons(x0, y1)) → ANDACTIVE(isNat(x0), isNatIListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2))
MARK(and(x1, x2)) → MARK(x1)
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(and(x1, x2)) → ANDACTIVE(mark(x1), mark(x2)) at position [0] we obtained the following new rules:

MARK(and(length(x0), y1)) → ANDACTIVE(lengthActive(mark(x0)), mark(y1))
MARK(and(take(x0, x1), y1)) → ANDACTIVE(takeActive(mark(x0), mark(x1)), mark(y1))
MARK(and(zeros, y1)) → ANDACTIVE(zerosActive, mark(y1))
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
MARK(and(uTake1(x0), y1)) → ANDACTIVE(uTake1Active(mark(x0)), mark(y1))
MARK(and(uLength(x0, x1), y1)) → ANDACTIVE(uLengthActive(mark(x0), x1), mark(y1))
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
MARK(and(nil, y1)) → ANDACTIVE(nil, mark(y1))
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
MARK(and(uTake2(x0, x1, x2, x3), y1)) → ANDACTIVE(uTake2Active(mark(x0), x1, x2, x3), mark(y1))
MARK(and(0, y1)) → ANDACTIVE(0, mark(y1))
MARK(and(cons(x0, x1), y1)) → ANDACTIVE(cons(mark(x0), x1), mark(y1))
MARK(and(s(x0), y1)) → ANDACTIVE(s(mark(x0)), mark(y1))
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(and(zeros, y1)) → ANDACTIVE(zerosActive, mark(y1))
MARK(s(x1)) → MARK(x1)
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
MARK(and(uTake1(x0), y1)) → ANDACTIVE(uTake1Active(mark(x0)), mark(y1))
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(uLength(x0, x1), y1)) → ANDACTIVE(uLengthActive(mark(x0), x1), mark(y1))
MARK(and(x1, x2)) → MARK(x1)
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(nil, y1)) → ANDACTIVE(nil, mark(y1))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(and(s(x0), y1)) → ANDACTIVE(s(mark(x0)), mark(y1))
MARK(and(cons(x0, x1), y1)) → ANDACTIVE(cons(mark(x0), x1), mark(y1))
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))
MARK(and(length(x0), y1)) → ANDACTIVE(lengthActive(mark(x0)), mark(y1))
MARK(and(take(x0, x1), y1)) → ANDACTIVE(takeActive(mark(x0), mark(x1)), mark(y1))
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
MARK(and(uTake2(x0, x1, x2, x3), y1)) → ANDACTIVE(uTake2Active(mark(x0), x1, x2, x3), mark(y1))
MARK(and(0, y1)) → ANDACTIVE(0, mark(y1))

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Narrowing

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(and(length(x0), y1)) → ANDACTIVE(lengthActive(mark(x0)), mark(y1))
MARK(and(take(x0, x1), y1)) → ANDACTIVE(takeActive(mark(x0), mark(x1)), mark(y1))
MARK(and(zeros, y1)) → ANDACTIVE(zerosActive, mark(y1))
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
MARK(and(uTake1(x0), y1)) → ANDACTIVE(uTake1Active(mark(x0)), mark(y1))
ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
MARK(and(uLength(x0, x1), y1)) → ANDACTIVE(uLengthActive(mark(x0), x1), mark(y1))
ANDACTIVE(tt, T) → MARK(T)
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(uTake2(x0, x1, x2, x3), y1)) → ANDACTIVE(uTake2Active(mark(x0), x1, x2, x3), mark(y1))
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNATLISTACTIVE(cons(N, L)) → ANDACTIVE(isNatActive(N), isNatListActive(L)) at position [0] we obtained the following new rules:

ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
ISNATLISTACTIVE(cons(x0, y1)) → ANDACTIVE(isNat(x0), isNatListActive(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Narrowing

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(and(zeros, y1)) → ANDACTIVE(zerosActive, mark(y1))
MARK(s(x1)) → MARK(x1)
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
MARK(and(uTake1(x0), y1)) → ANDACTIVE(uTake1Active(mark(x0)), mark(y1))
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
MARK(and(uLength(x0, x1), y1)) → ANDACTIVE(uLengthActive(mark(x0), x1), mark(y1))
ANDACTIVE(tt, T) → MARK(T)
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))
MARK(and(length(x0), y1)) → ANDACTIVE(lengthActive(mark(x0)), mark(y1))
MARK(and(take(x0, x1), y1)) → ANDACTIVE(takeActive(mark(x0), mark(x1)), mark(y1))
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
ISNATLISTACTIVE(cons(x0, y1)) → ANDACTIVE(isNat(x0), isNatListActive(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
MARK(and(uTake2(x0, x1, x2, x3), y1)) → ANDACTIVE(uTake2Active(mark(x0), x1, x2, x3), mark(y1))
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Narrowing

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ QDP

                                                                              ↳ Narrowing

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(and(zeros, y1)) → ANDACTIVE(zerosActive, mark(y1))
MARK(s(x1)) → MARK(x1)
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
MARK(and(uTake1(x0), y1)) → ANDACTIVE(uTake1Active(mark(x0)), mark(y1))
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(uLength(x0, x1), y1)) → ANDACTIVE(uLengthActive(mark(x0), x1), mark(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))
MARK(and(length(x0), y1)) → ANDACTIVE(lengthActive(mark(x0)), mark(y1))
MARK(and(take(x0, x1), y1)) → ANDACTIVE(takeActive(mark(x0), mark(x1)), mark(y1))
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
MARK(and(uTake2(x0, x1, x2, x3), y1)) → ANDACTIVE(uTake2Active(mark(x0), x1, x2, x3), mark(y1))
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(and(zeros, y1)) → ANDACTIVE(zerosActive, mark(y1)) at position [0] we obtained the following new rules:

MARK(and(zeros, y0)) → ANDACTIVE(cons(0, zeros), mark(y0))
MARK(and(zeros, y0)) → ANDACTIVE(zeros, mark(y0))

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Narrowing

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ QDP

                                                                              ↳ Narrowing

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
MARK(and(zeros, y0)) → ANDACTIVE(cons(0, zeros), mark(y0))
MARK(and(uTake1(x0), y1)) → ANDACTIVE(uTake1Active(mark(x0)), mark(y1))
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
MARK(and(uLength(x0, x1), y1)) → ANDACTIVE(uLengthActive(mark(x0), x1), mark(y1))
ANDACTIVE(tt, T) → MARK(T)
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))
MARK(and(length(x0), y1)) → ANDACTIVE(lengthActive(mark(x0)), mark(y1))
MARK(and(take(x0, x1), y1)) → ANDACTIVE(takeActive(mark(x0), mark(x1)), mark(y1))
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
MARK(and(uTake2(x0, x1, x2, x3), y1)) → ANDACTIVE(uTake2Active(mark(x0), x1, x2, x3), mark(y1))
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(zeros, y0)) → ANDACTIVE(zeros, mark(y0))

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Narrowing

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ QDP

                                                                              ↳ Narrowing

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ QDPOrderProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(and(length(x0), y1)) → ANDACTIVE(lengthActive(mark(x0)), mark(y1))
MARK(and(take(x0, x1), y1)) → ANDACTIVE(takeActive(mark(x0), mark(x1)), mark(y1))
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
MARK(and(uTake1(x0), y1)) → ANDACTIVE(uTake1Active(mark(x0)), mark(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
MARK(and(uLength(x0, x1), y1)) → ANDACTIVE(uLengthActive(mark(x0), x1), mark(y1))
ANDACTIVE(tt, T) → MARK(T)
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(uTake2(x0, x1, x2, x3), y1)) → ANDACTIVE(uTake2Active(mark(x0), x1, x2, x3), mark(y1))
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(and(take(x0, x1), y1)) → ANDACTIVE(takeActive(mark(x0), mark(x1)), mark(y1))

The remaining pairs can at least be oriented weakly.

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(and(length(x0), y1)) → ANDACTIVE(lengthActive(mark(x0)), mark(y1))
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
MARK(and(uTake1(x0), y1)) → ANDACTIVE(uTake1Active(mark(x0)), mark(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
MARK(and(uLength(x0, x1), y1)) → ANDACTIVE(uLengthActive(mark(x0), x1), mark(y1))
ANDACTIVE(tt, T) → MARK(T)
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(uTake2(x0, x1, x2, x3), y1)) → ANDACTIVE(uTake2Active(mark(x0), x1, x2, x3), mark(y1))
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₂
POL(ISNATILISTACTIVE(x₁)) = 0
POL(ISNATLISTACTIVE(x₁)) = 0
POL(MARK(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 0
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = 0
POL(isNatIListActive(x₁)) = 0
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = 0
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1
POL(takeActive(x₁, x₂)) = 1
POL(tt) = 0
POL(uLength(x₁, x₂)) = 0
POL(uLengthActive(x₁, x₂)) = 0
POL(uTake1(x₁)) = 0
POL(uTake1Active(x₁)) = 0
POL(uTake2(x₁, x₂, x₃, x₄)) = 0
POL(uTake2Active(x₁, x₂, x₃, x₄)) = 0
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

isNatActive(x1) → isNat(x1)
isNatIListActive(x1) → isNatIList(x1)
zerosActive → zeros
mark(zeros) → zerosActive
isNatListActive(x1) → isNatList(x1)
uTake1Active(x1) → uTake1(x1)
mark(uTake1(x1)) → uTake1Active(mark(x1))
takeActive(x1, x2) → take(x1, x2)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
andActive(x1, x2) → and(x1, x2)
zerosActive → cons(0, zeros)
uTake1Active(tt) → nil
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uLengthActive(tt, L) → s(lengthActive(mark(L)))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
isNatActive(length(L)) → isNatListActive(L)
mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatList(x1)) → isNatListActive(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(s(N)) → isNatActive(N)
andActive(tt, T) → mark(T)
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Narrowing

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ QDP

                                                                              ↳ Narrowing

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ QDPOrderProof

                                                                                        ↳ QDP

                                                                                          ↳ QDPOrderProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(and(length(x0), y1)) → ANDACTIVE(lengthActive(mark(x0)), mark(y1))
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
MARK(and(uTake1(x0), y1)) → ANDACTIVE(uTake1Active(mark(x0)), mark(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
MARK(and(uLength(x0, x1), y1)) → ANDACTIVE(uLengthActive(mark(x0), x1), mark(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
MARK(and(uTake2(x0, x1, x2, x3), y1)) → ANDACTIVE(uTake2Active(mark(x0), x1, x2, x3), mark(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(and(uTake1(x0), y1)) → ANDACTIVE(uTake1Active(mark(x0)), mark(y1))
MARK(and(uTake2(x0, x1, x2, x3), y1)) → ANDACTIVE(uTake2Active(mark(x0), x1, x2, x3), mark(y1))

The remaining pairs can at least be oriented weakly.

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(and(length(x0), y1)) → ANDACTIVE(lengthActive(mark(x0)), mark(y1))
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
MARK(and(uLength(x0, x1), y1)) → ANDACTIVE(uLengthActive(mark(x0), x1), mark(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₁
POL(ISNATILISTACTIVE(x₁)) = 1
POL(ISNATLISTACTIVE(x₁)) = 1
POL(MARK(x₁)) = 1
POL(and(x₁, x₂)) = 0
POL(andActive(x₁, x₂)) = 1
POL(cons(x₁, x₂)) = 0
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 1
POL(isNatIList(x₁)) = 1
POL(isNatIListActive(x₁)) = 1
POL(isNatList(x₁)) = 1
POL(isNatListActive(x₁)) = 1
POL(length(x₁)) = 1
POL(lengthActive(x₁)) = 1
POL(mark(x₁)) = 1
POL(nil) = 0
POL(s(x₁)) = 0
POL(take(x₁, x₂)) = 0
POL(takeActive(x₁, x₂)) = 0
POL(tt) = 1
POL(uLength(x₁, x₂)) = x₁
POL(uLengthActive(x₁, x₂)) = x₁
POL(uTake1(x₁)) = 0
POL(uTake1Active(x₁)) = 0
POL(uTake2(x₁, x₂, x₃, x₄)) = 0
POL(uTake2Active(x₁, x₂, x₃, x₄)) = 0
POL(zeros) = 0
POL(zerosActive) = 1

The following usable rules [17] were oriented:

isNatActive(x1) → isNat(x1)
isNatIListActive(x1) → isNatIList(x1)
zerosActive → zeros
mark(zeros) → zerosActive
isNatListActive(x1) → isNatList(x1)
uTake1Active(x1) → uTake1(x1)
mark(uTake1(x1)) → uTake1Active(mark(x1))
takeActive(x1, x2) → take(x1, x2)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
andActive(x1, x2) → and(x1, x2)
zerosActive → cons(0, zeros)
uTake1Active(tt) → nil
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uLengthActive(tt, L) → s(lengthActive(mark(L)))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
isNatActive(length(L)) → isNatListActive(L)
mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatList(x1)) → isNatListActive(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(s(N)) → isNatActive(N)
andActive(tt, T) → mark(T)
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Narrowing

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ QDP

                                                                              ↳ Narrowing

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ QDPOrderProof

                                                                                        ↳ QDP

                                                                                          ↳ QDPOrderProof

                                                                                            ↳ QDP

                                                                                              ↳ QDPOrderProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(and(length(x0), y1)) → ANDACTIVE(lengthActive(mark(x0)), mark(y1))
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
MARK(and(uLength(x0, x1), y1)) → ANDACTIVE(uLengthActive(mark(x0), x1), mark(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(and(length(x0), y1)) → ANDACTIVE(lengthActive(mark(x0)), mark(y1))
MARK(and(uLength(x0, x1), y1)) → ANDACTIVE(uLengthActive(mark(x0), x1), mark(y1))

The remaining pairs can at least be oriented weakly.

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₂
POL(ISNATILISTACTIVE(x₁)) = 0
POL(ISNATLISTACTIVE(x₁)) = 0
POL(MARK(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 0
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = 0
POL(isNatIListActive(x₁)) = 0
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = 1
POL(lengthActive(x₁)) = 1
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = x₂
POL(takeActive(x₁, x₂)) = x₂
POL(tt) = 0
POL(uLength(x₁, x₂)) = 1
POL(uLengthActive(x₁, x₂)) = 1
POL(uTake1(x₁)) = 0
POL(uTake1Active(x₁)) = 0
POL(uTake2(x₁, x₂, x₃, x₄)) = 0
POL(uTake2Active(x₁, x₂, x₃, x₄)) = 0
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

isNatActive(x1) → isNat(x1)
isNatIListActive(x1) → isNatIList(x1)
zerosActive → zeros
mark(zeros) → zerosActive
isNatListActive(x1) → isNatList(x1)
uTake1Active(x1) → uTake1(x1)
mark(uTake1(x1)) → uTake1Active(mark(x1))
takeActive(x1, x2) → take(x1, x2)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
andActive(x1, x2) → and(x1, x2)
zerosActive → cons(0, zeros)
uTake1Active(tt) → nil
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uLengthActive(tt, L) → s(lengthActive(mark(L)))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
isNatActive(length(L)) → isNatListActive(L)
mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatList(x1)) → isNatListActive(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(s(N)) → isNatActive(N)
andActive(tt, T) → mark(T)
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Narrowing

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ QDP

                                                                              ↳ Narrowing

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ QDPOrderProof

                                                                                        ↳ QDP

                                                                                          ↳ QDPOrderProof

                                                                                            ↳ QDP

                                                                                              ↳ QDPOrderProof

                                                                                                ↳ QDP

                                                                                                  ↳ QDPOrderProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(and(isNatIList(x0), y1)) → ANDACTIVE(isNatIListActive(x0), mark(y1))

The remaining pairs can at least be oriented weakly.

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₂
POL(ISNATILISTACTIVE(x₁)) = 1 + x₁
POL(ISNATLISTACTIVE(x₁)) = x₁
POL(MARK(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = x₁
POL(isNatIList(x₁)) = 1 + x₁
POL(isNatIListActive(x₁)) = 1 + x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = x₁
POL(length(x₁)) = x₁
POL(lengthActive(x₁)) = x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + x₁ + x₂
POL(takeActive(x₁, x₂)) = 1 + x₁ + x₂
POL(tt) = 0
POL(uLength(x₁, x₂)) = x₂
POL(uLengthActive(x₁, x₂)) = x₂
POL(uTake1(x₁)) = 0
POL(uTake1Active(x₁)) = 0
POL(uTake2(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄
POL(uTake2Active(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

isNatActive(x1) → isNat(x1)
isNatIListActive(x1) → isNatIList(x1)
zerosActive → zeros
mark(zeros) → zerosActive
isNatListActive(x1) → isNatList(x1)
uTake1Active(x1) → uTake1(x1)
mark(uTake1(x1)) → uTake1Active(mark(x1))
takeActive(x1, x2) → take(x1, x2)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
andActive(x1, x2) → and(x1, x2)
zerosActive → cons(0, zeros)
uTake1Active(tt) → nil
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uLengthActive(tt, L) → s(lengthActive(mark(L)))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
isNatActive(length(L)) → isNatListActive(L)
mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatList(x1)) → isNatListActive(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(s(N)) → isNatActive(N)
andActive(tt, T) → mark(T)
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Narrowing

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ QDP

                                                                              ↳ Narrowing

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ QDPOrderProof

                                                                                        ↳ QDP

                                                                                          ↳ QDPOrderProof

                                                                                            ↳ QDP

                                                                                              ↳ QDPOrderProof

                                                                                                ↳ QDP

                                                                                                  ↳ QDPOrderProof

                                                                                                    ↳ QDP

                                                                                                      ↳ QDPOrderProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ISNATILISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatIListActive(y1))
ISNATLISTACTIVE(cons(length(x0), y1)) → ANDACTIVE(isNatListActive(x0), isNatListActive(y1))

The remaining pairs can at least be oriented weakly.

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₂
POL(ISNATILISTACTIVE(x₁)) = x₁
POL(ISNATLISTACTIVE(x₁)) = x₁
POL(MARK(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = x₁
POL(isNatIList(x₁)) = x₁
POL(isNatIListActive(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = x₁
POL(length(x₁)) = 1 + x₁
POL(lengthActive(x₁)) = 1 + x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = x₁ + x₂
POL(takeActive(x₁, x₂)) = x₁ + x₂
POL(tt) = 0
POL(uLength(x₁, x₂)) = 1 + x₂
POL(uLengthActive(x₁, x₂)) = 1 + x₂
POL(uTake1(x₁)) = 0
POL(uTake1Active(x₁)) = 0
POL(uTake2(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄
POL(uTake2Active(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

isNatActive(x1) → isNat(x1)
isNatIListActive(x1) → isNatIList(x1)
zerosActive → zeros
mark(zeros) → zerosActive
isNatListActive(x1) → isNatList(x1)
uTake1Active(x1) → uTake1(x1)
mark(uTake1(x1)) → uTake1Active(mark(x1))
takeActive(x1, x2) → take(x1, x2)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
andActive(x1, x2) → and(x1, x2)
zerosActive → cons(0, zeros)
uTake1Active(tt) → nil
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uLengthActive(tt, L) → s(lengthActive(mark(L)))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
isNatActive(length(L)) → isNatListActive(L)
mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatList(x1)) → isNatListActive(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(s(N)) → isNatActive(N)
andActive(tt, T) → mark(T)
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Narrowing

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ QDP

                                                                              ↳ Narrowing

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ QDPOrderProof

                                                                                        ↳ QDP

                                                                                          ↳ QDPOrderProof

                                                                                            ↳ QDP

                                                                                              ↳ QDPOrderProof

                                                                                                ↳ QDP

                                                                                                  ↳ QDPOrderProof

                                                                                                    ↳ QDP

                                                                                                      ↳ QDPOrderProof

                                                                                                        ↳ QDP

                                                                                                          ↳ QDPOrderProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)
MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(and(isNatList(x0), y1)) → ANDACTIVE(isNatListActive(x0), mark(y1))

The remaining pairs can at least be oriented weakly.

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₂
POL(ISNATILISTACTIVE(x₁)) = 1 + x₁
POL(ISNATLISTACTIVE(x₁)) = 1 + x₁
POL(MARK(x₁)) = x₁
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = x₁
POL(isNatIList(x₁)) = 1 + x₁
POL(isNatIListActive(x₁)) = 1 + x₁
POL(isNatList(x₁)) = 1 + x₁
POL(isNatListActive(x₁)) = 1 + x₁
POL(length(x₁)) = 1 + x₁
POL(lengthActive(x₁)) = 1 + x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = x₁ + x₂
POL(takeActive(x₁, x₂)) = x₁ + x₂
POL(tt) = 0
POL(uLength(x₁, x₂)) = 1 + x₂
POL(uLengthActive(x₁, x₂)) = 1 + x₂
POL(uTake1(x₁)) = 0
POL(uTake1Active(x₁)) = 0
POL(uTake2(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄
POL(uTake2Active(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

isNatActive(x1) → isNat(x1)
isNatIListActive(x1) → isNatIList(x1)
zerosActive → zeros
mark(zeros) → zerosActive
isNatListActive(x1) → isNatList(x1)
uTake1Active(x1) → uTake1(x1)
mark(uTake1(x1)) → uTake1Active(mark(x1))
takeActive(x1, x2) → take(x1, x2)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
andActive(x1, x2) → and(x1, x2)
zerosActive → cons(0, zeros)
uTake1Active(tt) → nil
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uLengthActive(tt, L) → s(lengthActive(mark(L)))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
isNatActive(length(L)) → isNatListActive(L)
mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatList(x1)) → isNatListActive(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(s(N)) → isNatActive(N)
andActive(tt, T) → mark(T)
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatIListActive(zeros) → tt
isNatListActive(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ DependencyGraphProof

                                                  ↳ AND

                                                    ↳ QDP

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ Narrowing

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                                    ↳ QDP

                                                                      ↳ Narrowing

                                                                        ↳ QDP

                                                                          ↳ DependencyGraphProof

                                                                            ↳ QDP

                                                                              ↳ Narrowing

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ QDPOrderProof

                                                                                        ↳ QDP

                                                                                          ↳ QDPOrderProof

                                                                                            ↳ QDP

                                                                                              ↳ QDPOrderProof

                                                                                                ↳ QDP

                                                                                                  ↳ QDPOrderProof

                                                                                                    ↳ QDP

                                                                                                      ↳ QDPOrderProof

                                                                                                        ↳ QDP

                                                                                                          ↳ QDPOrderProof

                                                                                                            ↳ QDP

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
MARK(and(isNat(x0), y1)) → ANDACTIVE(isNatActive(x0), mark(y1))
MARK(and(and(x0, x1), y1)) → ANDACTIVE(andActive(mark(x0), mark(x1)), mark(y1))
ISNATILISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatIListActive(y1))
ISNATLISTACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
ISNATILISTACTIVE(cons(N, IL)) → ISNATILISTACTIVE(IL)
ANDACTIVE(tt, T) → MARK(T)
MARK(and(tt, y1)) → ANDACTIVE(tt, mark(y1))
ISNATLISTACTIVE(cons(0, y1)) → ANDACTIVE(tt, isNatListActive(y1))
ISNATILISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatIListActive(y1))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(s(x0), y1)) → ANDACTIVE(isNatActive(x0), isNatListActive(y1))
MARK(and(x1, x2)) → MARK(x2)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

ULENGTHACTIVE(tt, L) → LENGTHACTIVE(mark(L))
LENGTHACTIVE(cons(N, L)) → ULENGTHACTIVE(andActive(isNatActive(N), isNatListActive(L)), L)

The TRS R consists of the following rules:

mark(and(x1, x2)) → andActive(mark(x1), mark(x2))
andActive(x1, x2) → and(x1, x2)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(zeros) → zerosActive
zerosActive → zeros
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(uTake1(x1)) → uTake1Active(mark(x1))
uTake1Active(x1) → uTake1(x1)
mark(uTake2(x1, x2, x3, x4)) → uTake2Active(mark(x1), x2, x3, x4)
uTake2Active(x1, x2, x3, x4) → uTake2(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(uLength(x1, x2)) → uLengthActive(mark(x1), x2)
uLengthActive(x1, x2) → uLength(x1, x2)
mark(tt) → tt
mark(0) → 0
mark(s(x1)) → s(mark(x1))
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(nil) → nil
andActive(tt, T) → mark(T)
isNatIListActive(IL) → isNatListActive(IL)
isNatActive(0) → tt
isNatActive(s(N)) → isNatActive(N)
isNatActive(length(L)) → isNatListActive(L)
isNatIListActive(zeros) → tt
isNatIListActive(cons(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
isNatListActive(nil) → tt
isNatListActive(cons(N, L)) → andActive(isNatActive(N), isNatListActive(L))
isNatListActive(take(N, IL)) → andActive(isNatActive(N), isNatIListActive(IL))
zerosActive → cons(0, zeros)
takeActive(0, IL) → uTake1Active(isNatIListActive(IL))
uTake1Active(tt) → nil
takeActive(s(M), cons(N, IL)) → uTake2Active(andActive(isNatActive(M), andActive(isNatActive(N), isNatIListActive(IL))), M, N, IL)
uTake2Active(tt, M, N, IL) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → uLengthActive(andActive(isNatActive(N), isNatListActive(L)), L)
uLengthActive(tt, L) → s(lengthActive(mark(L)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We applied the Trivial transformation to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(take(N, IL)) → ISNAT(N)
ZEROS → ZEROS
TAKE(s(M), cons(N, IL)) → AND(isNat(N), isNatIList(IL))
TAKE(s(M), cons(N, IL)) → AND(isNat(M), and(isNat(N), isNatIList(IL)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(IL)
LENGTH(cons(N, L)) → ISNATLIST(L)
ISNATLIST(cons(N, L)) → AND(isNat(N), isNatList(L))
TAKE(s(M), cons(N, IL)) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
TAKE(s(M), cons(N, IL)) → ISNAT(M)
ISNATILIST(cons(N, IL)) → AND(isNat(N), isNatIList(IL))
TAKE(s(M), cons(N, IL)) → ISNAT(N)
ISNAT(length(L)) → ISNATLIST(L)
LENGTH(cons(N, L)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)
ISNATILIST(IL) → ISNATLIST(IL)
UTAKE2(tt, M, N, IL) → TAKE(M, IL)
LENGTH(cons(N, L)) → ULENGTH(and(isNat(N), isNatList(L)), L)
ISNATLIST(take(N, IL)) → ISNATILIST(IL)
TAKE(0, IL) → UTAKE1(isNatIList(IL))
ISNATLIST(cons(N, L)) → ISNATLIST(L)
ULENGTH(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → AND(isNat(N), isNatList(L))
TAKE(0, IL) → ISNATILIST(IL)
ISNAT(s(N)) → ISNAT(N)
ISNATLIST(cons(N, L)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNAT(N)
ISNATLIST(take(N, IL)) → AND(isNat(N), isNatIList(IL))

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(take(N, IL)) → ISNAT(N)
ZEROS → ZEROS
TAKE(s(M), cons(N, IL)) → AND(isNat(N), isNatIList(IL))
TAKE(s(M), cons(N, IL)) → AND(isNat(M), and(isNat(N), isNatIList(IL)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(IL)
LENGTH(cons(N, L)) → ISNATLIST(L)
ISNATLIST(cons(N, L)) → AND(isNat(N), isNatList(L))
TAKE(s(M), cons(N, IL)) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
TAKE(s(M), cons(N, IL)) → ISNAT(M)
ISNATILIST(cons(N, IL)) → AND(isNat(N), isNatIList(IL))
TAKE(s(M), cons(N, IL)) → ISNAT(N)
ISNAT(length(L)) → ISNATLIST(L)
LENGTH(cons(N, L)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)
ISNATILIST(IL) → ISNATLIST(IL)
UTAKE2(tt, M, N, IL) → TAKE(M, IL)
LENGTH(cons(N, L)) → ULENGTH(and(isNat(N), isNatList(L)), L)
ISNATLIST(take(N, IL)) → ISNATILIST(IL)
TAKE(0, IL) → UTAKE1(isNatIList(IL))
ISNATLIST(cons(N, L)) → ISNATLIST(L)
ULENGTH(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → AND(isNat(N), isNatList(L))
TAKE(0, IL) → ISNATILIST(IL)
ISNAT(s(N)) → ISNAT(N)
ISNATLIST(cons(N, L)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNAT(N)
ISNATLIST(take(N, IL)) → AND(isNat(N), isNatIList(IL))

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs with 13 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ZEROS → ZEROS

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ZEROS → ZEROS

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(take(N, IL)) → ISNAT(N)
ISNATLIST(cons(N, L)) → ISNAT(N)
ISNATLIST(cons(N, L)) → ISNATLIST(L)
ISNATILIST(cons(N, IL)) → ISNAT(N)
ISNAT(length(L)) → ISNATLIST(L)
ISNAT(s(N)) → ISNAT(N)
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)
ISNATILIST(IL) → ISNATLIST(IL)
ISNATLIST(take(N, IL)) → ISNATILIST(IL)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(take(N, IL)) → ISNAT(N)
ISNATLIST(cons(N, L)) → ISNAT(N)
ISNATLIST(cons(N, L)) → ISNATLIST(L)
ISNATILIST(cons(N, IL)) → ISNAT(N)
ISNAT(s(N)) → ISNAT(N)
ISNAT(length(L)) → ISNATLIST(L)
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)
ISNATILIST(IL) → ISNATLIST(IL)
ISNATLIST(take(N, IL)) → ISNATILIST(IL)

From the DPs we obtained the following set of size-change graphs:

ISNAT(length(L)) → ISNATLIST(L)
The graph contains the following edges 1 > 1
ISNAT(s(N)) → ISNAT(N)
The graph contains the following edges 1 > 1
ISNATLIST(cons(N, L)) → ISNATLIST(L)
The graph contains the following edges 1 > 1
ISNATILIST(IL) → ISNATLIST(IL)
The graph contains the following edges 1 >= 1
ISNATLIST(take(N, IL)) → ISNATILIST(IL)
The graph contains the following edges 1 > 1
ISNATILIST(cons(N, IL)) → ISNATILIST(IL)
The graph contains the following edges 1 > 1
ISNATILIST(cons(N, IL)) → ISNAT(N)
The graph contains the following edges 1 > 1
ISNATLIST(take(N, IL)) → ISNAT(N)
The graph contains the following edges 1 > 1
ISNATLIST(cons(N, L)) → ISNAT(N)
The graph contains the following edges 1 > 1

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ULENGTH(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → ULENGTH(and(isNat(N), isNatList(L)), L)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ULENGTH(tt, L) → LENGTH(L)
The graph contains the following edges 2 >= 1
LENGTH(cons(N, L)) → ULENGTH(and(isNat(N), isNatList(L)), L)
The graph contains the following edges 1 > 2

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

TAKE(s(M), cons(N, IL)) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
UTAKE2(tt, M, N, IL) → TAKE(M, IL)

The TRS R consists of the following rules:

and(tt, T) → T
isNatIList(IL) → isNatList(IL)
isNat(0) → tt
isNat(s(N)) → isNat(N)
isNat(length(L)) → isNatList(L)
isNatIList(zeros) → tt
isNatIList(cons(N, IL)) → and(isNat(N), isNatIList(IL))
isNatList(nil) → tt
isNatList(cons(N, L)) → and(isNat(N), isNatList(L))
isNatList(take(N, IL)) → and(isNat(N), isNatIList(IL))
zeros → cons(0, zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
uTake2(tt, M, N, IL) → cons(N, take(M, IL))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(L)), L)
uLength(tt, L) → s(length(L))

From the DPs we obtained the following set of size-change graphs:

UTAKE2(tt, M, N, IL) → TAKE(M, IL)
The graph contains the following edges 2 >= 1, 4 >= 2
TAKE(s(M), cons(N, IL)) → UTAKE2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)
The graph contains the following edges 1 > 2, 2 > 3, 2 > 4